A:Type, eq:EqDecider(A), ds:x:A fp Type, x:A. ds(x)?Void  ds(x)?Top 

latex

Definitions	EqDecider(T), f(x)?z, Unit, P  Q, P & Q, x  dom(f), a:A fp B(a), , Prop, b, A, b, f(x), x. t(x), x:A. B(x), P  Q, t  T, Top
Lemmas	top wf, fpf-ap wf, assert wf, not wf, bnot wf, bool wf, fpf-trivial-subtype-top, fpf-dom wf, assert of bnot, eqff to assert, iff transitivity, eqtt to assert, deq wf, fpf wf